fetch mcp.ax;
fetch mcp2.ax;
fetch mcp3.ax;
$;assume t0<t;
assume isconst(e);
∀e compile0 e t;
⊃e 2 3;
tauteq outcome(compile(e,t),load(xi))=outcome(mkli(val(e)),load(xi)),2;
tauteq outcome(compile(e,t),load(xi))=outcome(mkli(val(e)),load(xi)),4;
tauteq outcome(compile(e,t),load(xi))=outcome(compile(e,t),load(xi));
subst 4 in 5 occ 1;
cancel 6;
substr 4 in 5 occ 1;
cancel 6;
substr 4 in 5 occ 2;
∀e progsem1 mkli(val(e)) load(xi);
∀e li0 val(e);
⊃e 8 7;
∀e li1 val(e);
show proof;
subst 10 in 9;
∀e expsem0 e xi;
⊃e 2 12;
subst 13 in 11 occ 2;
tauteq outcome(compile(e,t),load(xi))=a(ac,value(e,xi),load(xi)),14 6;
∀e equiv0 a(ac,value(e,xi),load(xi));
cancel 16;
show proof;
∀e equiv0 t a(ac,value(e,xi),load(xi));
substr 15 in 16 occ 1;
cancel 17;
subst 15 in 16 occ 1;
⊃i 2 17;
assume isvar(e);
show proof;
∀e compile1 e t;
⊃e 19 20;
∀e progsem2 mkload(map(e)) load(xi);
∀e load0 map(e);
⊃e 22 23;
subst 21 in 24 occ 1;
∀e load1 map(e);
subst 26 in 25;
∀e map e xi;
⊃e 19 28;
substr 29 in 27;
∀e expsem1 e xi;
⊃e 19 31;
subst 32 in 30;
⊃i 33 19;
cancel 34;
⊃i 19 33;
cancel 34;
show proof;
∀e equiv0 t a(ac,value(e,xi),load(xi));
subst 33 in 34 occ 1;
⊃i 19 35;
$;